tg:Id, k:Knd, l:IdLnk, T, B:Type, f:(BT).
(rcv(l,tg) = k  T = B)
 @source(l): ma-single-sends0(B;T;k;l;tg;b.[f(b)])  Dsys
 & (D:Dsys.
 & (@source(l): ma-single-sends0(B;T;k;l;tg;b.[f(b)])  D
 & ( D 
 & ( realizes es.
 & ( (e:E. loc(e) = source(l)  Id  kind(e) = k  Knd  valtype(e)  B)
 & ( & (e:E. kind(e) = rcv(l,tg)  Knd  valtype(e)  T)
 & ( & (e:E.
 & ( & (loc(e) = source(l)  Id
 & ( & ( kind(e) = k  Knd
 & ( & ( (e':E.
 & ( & ( (kind(e') = rcv(l,tg)  Knd & sender(e') = e  E & val(e') = f(val(e))  T))) 

latex

Definitions	A & B, P & Q, P  Q, t  T, x:A. B(x), PossibleWorld(D;w), FairFifo, World, D1  D2, Dsys, D realizes es. P(es), Prop, rcv(l,tg), Knd, IdLnk, Id, ES(the_w), kind(e), source(l), loc(e), E, x:A. B(x), ||as||, Top, ij, val(e), valtype(e), b, sender(e), P  Q, P  Q, (x  l), hd(l), False, A, AB, 1of(t), {T}
Lemmas	es-kind-rcv, subtype rel self, hd wf, ge wf, member singleton, es-sender wf, es-val wf, non neg length, length wf1, length-map, es-E wf, es-loc wf, lsrc wf, es-kind wf, w-es wf, sends-rule0, Id wf, IdLnk wf, Knd wf, rcv wf, dsys wf, d-sub wf, world wf, fair-fifo wf, possible-world wf